\begin{tabbing}
EOrderAxioms($E$;${\it pred?}$;${\it info}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=($\forall$$e$:$E$, $l$:IdLnk.\+
\\[0ex]$\exists$\=${\it e'}$:$E$\+
\\[0ex]($\forall$${\it e''}$:$E$. 
\\[0ex]($\uparrow$rcv?(${\it e''}$))
\\[0ex]$\Rightarrow$ (sender(${\it e''}$) = $e$)
\\[0ex]$\Rightarrow$ (link(${\it e''}$) = $l$)
\\[0ex]$\Rightarrow$ (((${\it e''}$ = ${\it e'}$) $\vee$ ${\it e''}$ $<$ ${\it e'}$) $\wedge$ (loc(${\it e'}$) = destination($l$)))))
\-\\[0ex]$\wedge$ ($\forall$$e$,${\it e'}$:$E$. (loc($e$) = loc(${\it e'}$)) $\Rightarrow$ (${\it pred?}$($e$) = ${\it pred?}$(${\it e'}$)) $\Rightarrow$ ($e$ = ${\it e'}$))
\\[0ex]$\wedge$ SWellFounded(pred!($e$;${\it e'}$))
\\[0ex]$\wedge$ ($\forall$$e$:$E$. ($\neg$($\uparrow$first($e$))) $\Rightarrow$ (loc(pred($e$)) = loc($e$)))
\\[0ex]$\wedge$ ($\forall$$e$:$E$. ($\uparrow$rcv?($e$)) $\Rightarrow$ (loc(sender($e$)) = source(link($e$))))
\\[0ex]$\wedge$ \=($\forall$$e$,${\it e'}$:$E$.\+
\\[0ex]($\uparrow$rcv?($e$))
\\[0ex]$\Rightarrow$ ($\uparrow$rcv?(${\it e'}$))
\\[0ex]$\Rightarrow$ (link($e$) = link(${\it e'}$))
\\[0ex]$\Rightarrow$ sender($e$) $<$ sender(${\it e'}$)
\\[0ex]$\Rightarrow$ $e$ $<$ ${\it e'}$)
\-\-
\end{tabbing}